Nuprl Lemma : hd-filter 11,40

T:Type, P:(T), as:(T List).
(a:T. ((a  as) & (P(a))))
 ((hd(filter(a.P(a);as))  T)
 c ((hd(filter(a.P(a);as))  as) & (P(hd(filter(a.P(a);as)))))) 
latex


Definitionsx:AB(x), P  Q, x:AB(x), P & Q, x(s), t  T, hd(l), filter(P;l), reduce(f;k;as), if b then t else f fi , Y, , tt, ff, A c B, P  Q, {T}, , False, P  Q, Unit, P  Q, A,
Lemmasnil member, l member wf, assert wf, bool wf, eqtt to assert, iff transitivity, bnot wf, not wf, eqff to assert, assert of bnot, cons member

origin